COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.SS(Truth,,R8:)
C00016 00003	.SS(Computation)
C00022 00004	Suppose sentence %eP%1 is a proposed theorem of PC.  We consider ~%eP%1 and
C00038 ENDMK
C⊗;
.SS(Truth,,R8:)
An %3interpretation%1 consists of a non-empty set %6D%1, called the %3domain,
%1 and an assignment to each n-ary predicate letter %dA%4j%1 of an n-place 
relation in %6D%1; to each n-ary function letter %df%4j%1 of an n-place operation 
in %6D%1 (a function: %6D%8n%1→%6D%1); and to each individual constant 
?ai of some  fixed element of %6D%1.  Variables range over %6D%1 and the 
logical connectives ~, ⊃, and quantifiers ∀, ∃ are given their usual meaning.

For a given interpretation, a wff without free variables (called a %3closed%1
wff) represents a statement which is true or false.  A wff with free variables
represents a relation on the domain which may be true for some values of the
free variables and false for others.  The ideas of satisfiability and truth
can be made precise in the following way.

.BEGIN "at";
.at "?s1"⊂"%6s%41%1"⊃
.at "?sk"⊂"%6s%4k%1"⊃
.at "?s"⊂"%6s%1"⊃
.at "?g"⊂"%6g%1"⊃

Let there be given an interpretation with domain %6D%1.  Let %gS%1 be the set
of denumerable sequences of elements of %6D%1.  We want to define what it means
for a sequence ?s=(?b1, ?b2, ...) in %gS%1 to safisfy a wff %eA%1 under the given
interpretation.  First we define a function ?s* of one argument, with terms as
arguments and values in %6D%1.
.BEGIN NOFILL;
1) if ?t is ?xi, then ?s*(?t)=?bi
2) if ?t is an individual constant, then ?s*(?t) is the fixed element of %6D%1
assigned to that constant by the interpretation
3) if ?fj is a function letter and ?g is the corresponding operation in %6D%1,
and ?t1, ..., ?tn are terms, then ?s*(?fj(?t1, ..., ?tn))=?g(?s*(?t1), ..., ?s*(?tn))
.END

Thus ?s* is a function, determined by the sequence ?s, from the set of terms
into %6D%1.  Intuitively, for a sequence ?s=(?b1, ?b2, ...) and a term ?t, ?s*(?t) 
is the element of %6D%1 obtained by substituting, for each  i, ?bi for all
occurrences of ?xi in ?t, and then performing the operations of the interpretation 
corresponding to the function letters of ?t, e.g. if ?t is ?f2(?x3,?f1
(?x1,?a1)) and the interpretation is such that %6D%1=set of integers, ?f2 and
?f1 are assigned to ordinary multiplication and addition, resp., and ?a1 is 
the constant 2, then for any sequence of integers ?s=(?b1, ?b2, ...), ?s*(?t) is
the integer ?b3(?b1+2).
.BEGIN indent 10,10;

i) If %eA%1 is an atomic wff %dA%4j%1(?t1, ..., ?tn) and %6A%4j%1 is the 
corresponding 
relation of the interpretation, then the sequence ?s %3satisfies%1 %eA%1 iff 
%6A%4j%1(?s*(?t1), ..., ?s*(?tn)), that is if the n-tuple (?s*(?t1), ..., ?s*(?tn))
is in the relation %6A%4j%1⊗↓you should understand the difference between %eA%1,
%dA%1, and %6A%1!←

ii) ?s %3satisfies%1 ~%eA%1 iff ?s does not satisfy %eA%1

iii) ?s %3satisfies%1 %eA%1⊃%eB%1 iff either ?s does not satisfy %eA%1, or ?s 
satisfies %eB%1

iv) ?s %3satisfies%1 (∀?xi)%eA%1 iff every sequence of %gS%1 which differs from
?s in at most the ith component satisfies %eA%1.
.END

Intuitively, a sequence ?s=(?b1,?b2,...) satisfies a wff %eA%1 iff when we
substitute ?bi for all free occurrences of ?xi in %eA%1, for every i, the resulting
proposition is true under the given interpretation.
.group;
A wff %eA%1 is %3true%1 (for a given interpretation) iff every sequence in %gS%1
satisfies %eA%1.
%eA%1 is %3false%1 iff no sequence in %gS%1 satisfies %eA%1.
An interpretation is said to be a %3model%1 for a set %gG%1 of wffs iff every wff
in %gG%1 is true for the interpretation. Consequences of the above definitions
follow:
.BEGIN indent 3,3;
1) %eA%1 is false for a given interpretation iff ~%eA%1 is true for that
interpretation; and %eA%1 is true iff ~%eA%1 is false.

2) If %eA%1 and %eA%1⊃%eB%1 are true for a given interpretation, so is %eB%1.

3) For a given interpretation %eA%1⊃%eB%1 is false iff %eA%1 is true and %eB%1
is false.
.apart
4) ?s satisfies %eA%1∧%eB%1 iff ?s satisfies %eA%1 and ?s satisfies %eB%1;
   ?s satisfies %eA%1∨%eB%1 iff ?s satisfies %eA%1 or ?s satisfies %eB%1;
   ?s satisfies %eA%1≡%eB%1 iff ?s satisfies both %eA%1 and %eB%1, or, neither
   %eA%1 nor %eB%1;
   ?s satisfies (∃?x)%eA%1 iff there exists a sequence ?s' differing from ?s in at most the
   ith place such that ?s' satisfies %eA%1.

5) %eA%1 is true iff its closure (∀?x)%eA%1 is true.  By the %3closure%1 of %eA%1
we mean the closed wff obtained from %eA%1 by prefixing as universal quantifiers
those variables which appear free in %eA%1.

.P13:
6) Every instance of a tautology is true for any interpretation.  (All instances
of the axioms %7A1-A3%1 are true.  By 3) above, if %eA%1 and %eA%1⊃%eB%1 are true
then so is %eB%1, thus using completeness for propositional logic, we have every
instance of a tautology (or theorem of propositional logic) is true.)

.P6:
7) If the free variables (if any) of a wff %eA%1 occur in the list ?x1, ..., ?xk and
if the sequences ?s and ?s' have the same components in the 1st, ..., kth places,
then ?s satisfies %eA%1 iff ?s' satisfies %eA%1.  
.BEGIN INDENT 5,5;
Corollary:  If %eA%1 is a closed
wff, then for any given interpretation and any two sequences ?s and ?s', ?s 
satisfies %eA%1 iff ?s' satisfies %eA%1.  Thus for a given interpretation
either %eA%1 is true or ~%eA%1 is true (i.e. %eA%1 is false).
.END

8) If ?t and ?u are terms and ?s is a sequence in %gS%1, and ?t' results from ?t
by substitution of ?u for all occurrences of ?xi in ?t, and ?s' results from ?s by
substituting ?s*(?u) for the ith component of ?s, then ?s*(?t')=(?s')*(?t) for
sketch of proof see Mendelson [ ]).
                                        
.BEGIN INDENT 5,5;
Corollary:  If (∀?xi)%eA%1(?xi) is satisfied
by ?s, so is %eA%1(?t).  Hence (∀?xi)%eA%1(?xi)⊃%eA%1(?t) is true for all 
interpretations.
.end

9) If %eA%1 does not contain ?xi free, then (∀?xi)(%eA%1⊃%eB%1)⊃(%eA%1⊃(∀?xi)%eB%1)
is true for all interpretations.  (For proof see Mendelson [ ])
.END
.end "at"

A wff %eA%1 is said to be %3logically%1 %3valid%1 iff %eA%1 is true for every
interpretation.

%eA%1 is said to be %3satisfiable%1 iff there is an interpretation for which
%eA%1 is satisfied by at least one sequence in %gS%1.

Thus %eA%1 is logically valid iff ~%eA%1 is unsatisfiable; and %eA%1 is
satisfiable iff ~%eA%1 is not logically valid.  If ?A is a closed wff, then
?A is either true or false for any given interpretation, i.e. ?A is satisfied
by all sequences or by none, thus if ?A is closed, then ?A is satisfiable iff
?A is true for some interpretation.

?A is %3contradictory%1 (unsatisfiable) iff ~?A is logically valid, i.e., iff
?A is false for every interpretation.

?A is said to %3logically imply%1 ?B iff, in every interpretation, any sequence
satisfying ?A also satisfies ?B.  ?B is a %3logical consequence%1 of a set %gG%1
of wffs iff, in every interpretation, every sequence which satisfies every wff
in %gG%1 also satisfies ?B.  

?A and ?B are %3logically equivalent%1 iff they
logically imply each other.  Immediate consequences of the above definitions
are:
.BEGIN indent 10,10;fill;
a) ?A logically implies ?B iff ?A⊃?B is logically valid.

b) ?A and ?B are logically equivalent iff ?A≡?B is logically valid.

c) If ?A logically implies ?B, and ?A is true in a given interpretation, then  so is ?B.

d) If ?B is a logical consequence of a set %gG%1 of wffs, and all wffs in %gG%1  are true in a 
      given interpretation, so is ?B.
.END

Any sentence of a formal language which is an instance of a logically valid wff
is called %3logically true%1, and an instance of a contradictory wff is said
to be %3logically false%1.  The following properties are immediate:
.BEGIN NOFILL;

	i) Every instance of a tautology is logically valid.  
	  By definition and 6) of previous remarks, {yon (P6)}.
	ii) If ?A does not contain ?x free, then (∀?x)(?A⊃?B)⊃(?A⊃(∀?x)?B) is logically valid.
	   By 9) of previous remarks
	iii) If ?t is free for ?x in ?A, then (∀?x)?A(?x)⊃?A(?t) is logically valid.
	     By corollary to 8) of previous remarks
	iv) The wff (∀?x2)(∃?x1)%dA%41%1(?x1,?x2)⊃(∃?x1)(∀?x2)%dA%41%1(?x1,?x2) is not logically valid.
	   counterexample: 
	  	%6D%1 is the set of integers ;%dA%41%1(?x1,?x2) is ?x1<?x2

		Then (∀?x2)(∃?x1)%dA%41%1(?x1,?x2) is true,
		i.e., for every integer ?x2, there exists another integer ?x1, such that ?x1<?x2.
		However, (∃?x1)(∀?x2)%dA%41%1(?x1,?x2) is false,
		i.e., there does not exist a least integer.
.end


.SS(Computation)
In describing the process of computation for the propositional case we
discussed ground resolution.  A %3ground%1 expression, term or clause,
is one which contains no variables.  For the predicate calculus we use a more
general form of resolution which consists of substitution and complementary
literal elimination.  Again, we shall use refutation procedures establishing a 
theorem by showing its negation is inconsistent.  Since in PC we have 
introduced some new symbols, we re-define some notions and add some as 
follows.
.BEGIN NOFILL;
.turnoff "{","}";
	<term>:= <variable> | <function letter>(<term>%41%1,...,<term>%4n%1) 
	<atomic formula>:= <predicate letter>(<term>%41%1,...,<term>%4n%1)  
	<literal>:= <atomic formula> | ~<atomic formula>
	<clause>:= %5b%1 | {<literal>} | {<literal>} ∪ <clause>
	<sentence>:= {<clause>} | <sentence> ∪ {<clause>}
.turnon "{","}";
.end
Again, we understand a clause to be a disjunction of its elements, a sentence
to be a conjunction of its elements.

Resolution depends on the basic operation of substituting terms for variables
in wffs.  To make this notion precise we introduce the following definitions.
If a variable ?v is replaced at each of its occurrences in the wff ?C by the
term ?t, the resulting wff is called a %3substitution instance%1 of ?C, and
is denoted ?C[(?t,?v)].  Similarly, the result of %3simultaneously%1 replacing
all occurrences of different variables ?v1, ..., ?vn in ?C by terms ?t1, ..., ?tn
respectively, is denoted by ?C[(?t1,?v1), ..., (?tn,?vn)].  A %3substitution %gs%1
.turnoff "{","}";
is a set of ordered pairs (we use "[" and "]" instead of "{" and "}" for 
substitutions) %gs%1=[(?t1,?v1), ..., (?tn,?vn)], the first element of each
pair being a term and the second element a variable, such that ?vi≠?vj and ?ti≠?vi.
The result of applying %gs%1 to ?C, ?C%gs%1 is the substitution instance
?C[(?t1,?v1), ..., (?tn,?vn)].
.turnon "{","}";
.begin nofill;
		ex.  %dC = P(x, z, y)∨P(e, f(u,y), f(a,b))
		     %gs%d = [(e,x), (f(u,y),z), (f(a,b),y)]
		     %gt%d = [(f(a,b),y)]
		     C%gs%d = P(e, f(u,y), f(a,b)) ∨ P(e, f(u,f(a,b)), f(a,b))
		     (C%gs%d)%gt%d = P(e, f(u,f(a,b)), f(a,b))
.end

The condition ?ti≠?vi ensures that two substitutions are set-theoretically
equal iff they have the same effect on all well-formed expressions.  The
notation %6P%1(%6S%1) denotes the set of instances obtained by applying
to a set %6S%1 of wffs all substitutions with terms belonging to a set
%6P%1 of terms.

We assume that the wffs and sequences of wffs have the lexical ordering defined
as follows:
.BEGIN INDENT 10,10;
a) The primitive symbols are ordered according to type (variables, functions,
predicates, then connectives) and then within each type according to number
of arguments (for functions and predicates), then subscripts, and finally
by alphabetical order.

b) Wffs are ordered first by length, and then two wffs of equal length are
placed in the order of their ith pair of symbols if they differ first at
the ith position.  Similarly, sequences of wffs are ordered by length and
then by the order of the first members which differ.
.end
.begin indent 15,15;
for example: ?x1 comes before ?y1 comes before ?x3; %df(f(x))%1 before %df(f(y));
f(y)%1 before %dg(x); f(g%41%d(y))%1 before %df(f%42%d(x))%1, etc.
.end

Suppose sentence %eP%1 is a proposed theorem of PC.  We consider ~%eP%1 and
assume it is in %3prenex form%1 (every variable quantified⊗↓we first
form the %3closure%* of ~?P by universally quantifying all free variables;
by 5){yon(P6)} we know ~?P is true iff its closure is true.←,
and all quantifiers precede a quantifier-free
sentence), and that the quantifier-free sentence is in reduced conjunctive form.
For example, consider:

.begin center;
~?P = (∃?x1)(∀?x2)(∃?x3)(∀?x4)%dR%1(?x1,?x2,?x3,?x4)
.end

First, each existentially quantified variable is replaced by a Skolem function
of the universally quantified variables governing it, (a 0-ary function being
a constant) and the universal quantifiers are dropped, yielding

.begin center;
?P' = %dR%1(?a, ?x2, ?f(?x2), ?x4)
.end

This is 
called %3Skolem free variable form%1.  
Clearly, ~?P is satisfiable (has a model) iff ?P' is satisfiable, since
?P' logically implies ~?P, and if ~?P is true in some interpretation with
domain ?D, then there are functions over ?D satisfying ?P'.  
Note that ?P' is a finite conjunction
of clauses, each of which is a disjunction of atomic formulae.

Consider the set of terms, ?H, obtained from ?P' by
.begin indent 10,10;
.begin nofill;
1) if ?a is a constant (or, 0-ary function symbol) in ?P' then ?aε?H
.end
2) if ?a1, ..., ?an are terms in ?H, and ?f is an n-ary function symbol
in ?P' then ?f(?a1,...,?an)ε?H.  If ?P' has no constants an arbitrary constant ?a is included in ?H.  
We call ?H the %3Herbrand domain%1 of ?P'.  The set of all substitution instances
of ?P', obtainable by replacing each variable in ?P' by a term from ?H, is
called the %3Herbrand expansion%1 of ?P', denoted ?H(?P').  For example:
.begin tabit3(20,28,36);
\?x2\?x3\%dR%1(?a, ?x2, ?f(?x2), ?x3)
\________________________________________
\?a\?a\%dR%1(?a, ?a, ?f(?a), ?a)
\?a\?f(?a)\%dR%1(?a, ?a, ?f(?a), f(a))
\?f(?a)\?a\%dR%1(?a, ?f(?a), ?f(?f(?a)), ?a)
\?a\?f(?f(?a))\%dR%1(?a, ?a, ?f(?a), ?f(?f(?a)))
\...\...\ ...
\where ?x2, and ?x3 are replaced in all possible ways by the terms 
\?a, ?f(?a), ?f(?f(?a)), ?f(?f(?f(?a))), ... in ?H, each variable
\being replaced in all of its occurrences by the same term.
.end
.end

At certain intervals we can test the conjunction of the instances so far
generated for inconsistency.  If this conjunction is consistent, we
generate further instances and test the larger conjunction, and continue
in this way until an inconsistent set of instances is found.  That this
will happen precisely in the case that ?P' is unsatisfiable (and hence,
our original ?P is a theorem) follows from Herbrand's Theorem.

%7THEOREM 5%1 (Herbrand's Theorem)
If ?P is a finite conjunction of clauses, and ?H is its Herbrand domain,
then ?P is unsatisfiable iff some finite subset of ?H(?P) is inconsistent.
(proof omitted)

The problem with testing subsets of ?H(?P), is not the time taken to test 
a subset, but that if ?H(?P) is generated according to the increasing
complexity of the ground terms in the instances, a prohibitively large
number of instances may have to be generated before an inconsistent conjunction
arises.  If ?P is simple, then a small inconsistent sub-conjunction can 
be found.  Therefore the problem is to avoid generating the consistent
instances.  One way to do this is to "predict" which instances of two
clauses will contain complementary literals (or, will "clash") using
the information we have at hand about the way in which the terms of the
Herbrand domain are constructed.  For example, suppose that the clauses
of ?J are

.begin nofill;
		1) %dP(x, e, x)%1
  		2) %d~P(y, z, v) ∨ ~P(y, v, w) ∨ P(e, z, w)%1
		3)%d P(a, f(u,v), e)%1
		4) %d~P(e, f(f(b,c),a), a)%1
		where %da, b, c, e%1 are constants
.end

Any instance of 1) will clash with any instance of 2) in which %dv%1 is 
replaced by %de%1, and %dy%1 and %dw%1 are replaced by the term which
replaces ?x in 1); such an instance will have the form

.begin center;
%d~P(x, z, e) ∨ ~P(x, e, x) ∨ P(e, z, x)%1
.end

Thus there will be a family of resolvents of instances of 1) and 2) of the 
form
.begin center;
5) %d~P(x, z, e) ∨ P(e, z, x)%1
.end

Some of these will clash with instances of 3), namely those instances of 5)
of the form 
.begin center;
%d~P(a, f(u,v), e) ∨ P(e, f(u,v), a)%1
the resolvents being
6) %dP(e, f(u,v), a)%1
.end

This family contains the clause
.begin center;
7) %dP(e, f(f(b,c),a), a)%1
.end
which clearly contradicts 4).  Thus a small segment of ?H(?J) is contradictory;
if ?H(?J) is generated by the usual method, the first contradictory segment 
would contain between 4%86%1 and 20%86%1 clauses.

Such arguments involve applying a succession of substitutions of terms (not necessarily
ground terms) for variables, each substitution being chosen so that the 
result of applying it to two clauses is that some of the literals in the 
first clause become equal (or collapse) to a literal ?L and some of the
literals in the second clause collapse to ~?L.  
In order to formalize these arguments we introduce: 1) composition of
substitutions, 2) the concept of a "unifying substitution", and 3) the
concept of a "most general substitution" having a given property.

Let %gq%1,%gy%1 be substitutions.  The %3composition%1 of ?q and %gy%1, denoted
?q%gy%1, is the substitution defined as follows:
.begin nofill;
		Let  ?q = [(?t1,?v1), ..., (?tn,?vn)]
		     ?q' = [(?t1%gy%1, ?v1), ..., (?tn%gy%1, ?vn)] , such that ?ti%gy%1≠?vi,
.end
and let %gy%1  consist of those pairs of %gy%1 whose second elements do not occur 
among the variables ?v1,#...,#?vn of ?q, say
.begin nofill;
		     %gy%1' = [(?s1, ?u1), ..., (?sk, ?uk)]
		Then ?q%gy%1 = ?q' ∪ %gy%1'
.end
 
Remark: The result of applying ?q and %gy%1 successively to a wff ?C is the same 
as applying ?q%gy%1.  That is, (?C?q)%gy%1 = ?C(?q%gy%1).  Furthermore, 
composition of substitutions is associative, (?q%gs%1)%gy%1 = ?q(%gsy%1).
.begin turnoff "{","}";

Let ?L = {%dL%41%d, L%42%d, ..., L%4n%1} be a set of literals.  ?L is
%3unified%1 by %gs%1 if %dL%41%gs%1 = %dL%42%gs%1 = ... = %dL%4n%gs%1.
Clearly, if %gs%1 unifies ?L, so does %gst%1 where %gt%1 is any substitution.

?q is a %3most general substitution%1 satisfying a condition %6C%1 if for
any %gs%1 satisfying %6C%1 there is a substitution %gl%1 such that 
%gs%1 = %gql%1.

Intuitively, a most general substitution is one which makes the fewest and
most general (in the sense of leaving variables wherever possible) 
substitutions necessary to satisfy the given condition.  In many cases there
will be no most general substitution satisfying the given condition.
However, if a set ?L of literals is unifiable, then there is a most general
substitution unifying ?L and, moreover, we can give an algorithm for
finding such a substitution.  This procedure, due to Robinson, starts
with the empty substitution and builds up, step by step, a most general
?s0 which unifies the set ?L of literals.  If, at the kth step, the
substitution so far obtained is %gs%4k%1, and the literals %dL%41%gs%4k%1, ...,
%dL%4n%gs%4k%1 in ?L%gs%4k%1 are not all equal, the procedure changes
%gs%4k%1 on the basis of a "disagreement list" containing the first
well-formed expression in each ?L%4i%gs%4k%1 which needs to be changed.

Consider each %dL%4i%gs%4k%1 to be a sequence of symbols.  Define the
%3disagreement set%1 of ?L%gs%4k%1 to be the set of all well-formed
sub-expressions of the literals in ?L%gs%4k%1 which begin at the first
symbol position at which not all the literals have the same symbol.
This set is either ?L itself (in which case ?L is not unifiable) or else
it contains a term or subterm from each literal in ?L%gs%4k%1.

.begin center;fill
		ex. the disagreement set of %d{P(x, f(x,g(y)), v), P(x, f(x,z), w)}
		   is  {z, g(y)}
.end
.end

Robinson's unification procedure is as follows:
.begin indent 6,6;
1) Set %gs%41%1 = %gf%1 (the empty substitution), set k=0, and go to 2)

2) Set k=k+1.  If the elements of ?L%gs%4k%1 are all equal, set ?s0 = %gs%4k%1
and stop; otherwise go to 3).

3) Let ?sk, ?tk be the two earliest expressions in the lexical ordering of
the disagreement set of ?L%gs%4k%1; if ?sk is a variable and does not
occur in ?tk, set %gs%4k+1%1 = %gs%4k%1[(?tk,?sk)] and go to 2); otherwise
stop.
.end

Since ?L%gs%4k+1%1 contains one less variable than ?L%gs%4k%1, the procedure
must stop in at most m steps if ?L has m  variables.
Also, it is clear that if the procedure stops at stage 2), ?s0 is uniquely
determined and its terms contain only function symbols occurring in ?L.  It
is also true that if ?L is unifiable then ?s0 is defined and is a most
general substitution.  For a proof of this statement see Luckham [ ].

Finally we are in a position to extend the concept of a resolvent of two
clauses to the case where the clauses are not necessarily ground clauses.

A %3 resolvent of two clauses ?C1 and ?C2 is a third clause ?C3 obtained as
follows:
.begin indent 10,10;
1) If ?v1, ..., ?vm are the variables of ?C2, and the highest variable of
?C1 in the lexical order is ?uk, let ?q = [(?u%4k+1%1, ?v1), ..., 
(?u%4k+m%1, ?vm)].  (Thus, none of the variables in ?C2?q occurs in ?C1.)
.turnoff "{", "}";

2) If there is a pair of sets of literals, ?L = {%dL%41%1, ..., %dL%4k%1} and
%eM%1 = {%dM%41%1, ..., %dM%4n%1} such that ?L⊂?C1, %eM%1⊂?C2 and the set
{%dL%41%1, ..., %dL%4k%1, %dM%41%1?q, ..., %d~M%4n%1?q} is unifiable, 
.turnon "{", "}";
let
?s0 be the most general unifying substitution (chosen by the procedure
above) so that ?L?s0 and %eM%1?q?s0 are complementary literals⊗↓actually,
they are singleton sets whose elements are complementary literals←; then
?C3 is the set of the literals: (?C1-?L)?s0 ∪ (?C2-%eM%1)?q?s0
.END